i, x:Id, k:Knd, ds:x:Id fp Type, T:Type, f:(State(ds)Tds(x)?Void).
((isrcv(k))  (i = destination(lnk(k))))
 @i: with declarations 
 ds:ds
 da:k : T

 effect of k(v) is x := f s v 
 realizes es.
 @i events of kind k change continuous x to f State(ds) (val:T) 

latex

Definitions

t  T, x:A. B(x), P  Q, Void, x:A.B(x), Top, KindDeq, Knd, {T}, SQType(T), s = t, , s ~ t, left + right, Atom$n, Id, x:A  B(x), a:A fp B(a), Type, x:AB(x), Dsys, D1  D2, World, P & Q, FairFifo, PossibleWorld(D;w), t.1, E, f(x)?z, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), x.A(x), x. t(x), valtype(e), "$token", let x,y = A in B(x;y), f(a), , t.2, a(i;t), isnull(a), b, A, {x:A| B(x)} , loc(e), (timed)state after e, <a, b>, , A c B, P  Q, P  Q, a = b, e@i. P(e), isrcv(k), destination(l), kindtype(i;k), @i events of kind k change continuous x to f State(ds) (val:T), S  T, IdDeq, State(ds), suptype(S; T), @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, D realizes es. P(es), lnk(k), ES(the_w), kind(e), x : v, Valtype(da;k)

Lemmas

effect-rule, fpf wf, ldst wf, lnk wf, dsys wf, d-sub wf, d-single-effect wf, ma-state wf, rationals wf, fpf-cap wf, id-deq wf, world wf, fair-fifo wf, possible-world wf, isrcv wf, assert-eq-id, assert-eq-knd, es-kind wf, es-loc wf, not wf, assert wf, w-isnull wf, w-a wf, pi1 wf, pi2 wf, nat wf, Id wf, subtype rel transitivity, es-valtype wf, w-es wf, ma-valtype wf, fpf-single wf, fpf-cap-single, Knd sq, fpf-cap-single1, Knd wf, Kind-deq wf, subtype rel self